ecl-trans-reachable(ds;da;v;L;x)
== let T,ks,i,g,h,a,e = v in 
== L':event-info(ds;da) List
== (L'  L
== c ((||L'|| < ||L||)
== c & x
== c & =
== c & list_accum(x,a.let k,zz = a
== c & list_accum(x,a.in
== c & list_accum(x,a.let s,v = zz in if deq-member(KindDeq;k;ks) then g(k,s,v,x) else x fi ;
== c & list_accum(i;
== c & list_accum(L'))) 

latex

---

clarification:

ecl-trans-reachable(ds;da;v;L;x)
== let T,ks,i,g,h,a,e = v in 
== L':event-info(ds;da) List
== (L'  L  event-info(ds;da) List
== c ((||L'|| < ||L||)
== c & x
== c & =
== c & list_accum(x,a.let k,zz = a
== c & list_accum(x,a.in
== c & list_accum(x,a.let s,v = zz in if deq-member(KindDeq;k;ks) then g(k,s,v,x) else x fi ;
== c & list_accum(i;
== c & list_accum(L')
== c &  T)) 

latex

Definitions	let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), x:A. B(x), A c B, l1  l2, event-info(ds;da), P & Q, ||as||, list_accum(x,a.f(x;a);y;l), if b then t else f fi , deq-member(eq;x;L), KindDeq
FDL editor aliases	ecl-trans-reachable